Problem:
 a(b(c(x1))) -> a(a(b(x1)))
 a(b(c(x1))) -> b(c(b(c(x1))))
 a(b(c(x1))) -> c(b(c(a(x1))))

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    c3(187) -> 188*
    c3(182) -> 183*
    c3(172) -> 173*
    c3(147) -> 148*
    c3(139) -> 140*
    c3(141) -> 142*
    c3(185) -> 186*
    c3(170) -> 171*
    c3(145) -> 146*
    c1(31) -> 32*
    c1(16) -> 17*
    c1(33) -> 34*
    c1(28) -> 29*
    c1(18) -> 19*
    b3(162) -> 163*
    b3(142) -> 143*
    b3(186) -> 187*
    b3(171) -> 172*
    b3(166) -> 167*
    b3(146) -> 147*
    b3(126) -> 127*
    b3(173) -> 174*
    b3(140) -> 141*
    b1(32) -> 33*
    b1(17) -> 18*
    b1(19) -> 20*
    b1(14) -> 15*
    b1(4) -> 5*
    a3(127) -> 128*
    a3(184) -> 185*
    a3(164) -> 165*
    a3(144) -> 145*
    a3(196) -> 197*
    a3(163) -> 164*
    a3(128) -> 129*
    a1(30) -> 31*
    a1(5) -> 6*
    a1(42) -> 43*
    a1(6) -> 7*
    c2(65) -> 66*
    c2(97) -> 98*
    c2(52) -> 53*
    c2(109) -> 110*
    c2(54) -> 55*
    c2(111) -> 112*
    c2(86) -> 87*
    c2(63) -> 64*
    c2(100) -> 101*
    c2(95) -> 96*
    a0(2) -> 3*
    a0(1) -> 3*
    b2(55) -> 56*
    b2(84) -> 85*
    b2(74) -> 75*
    b2(64) -> 65*
    b2(44) -> 45*
    b2(96) -> 97*
    b2(76) -> 77*
    b2(98) -> 99*
    b2(53) -> 54*
    b2(130) -> 131*
    b2(110) -> 111*
    b0(2) -> 1*
    b0(1) -> 1*
    a2(45) -> 46*
    a2(77) -> 78*
    a2(62) -> 63*
    a2(156) -> 157*
    a2(106) -> 107*
    a2(46) -> 47*
    a2(108) -> 109*
    a2(120) -> 121*
    c0(2) -> 2*
    c0(1) -> 2*
    1 -> 42,28,14
    2 -> 30,16,4
    7 -> 78,109,62,6,43,3
    15 -> 5*
    16 -> 120,100,84
    18 -> 62,52,44
    20 -> 78,109,62,6,43,3
    28 -> 108,95,76
    29 -> 17*
    34 -> 78,109,62,6,43,3
    43 -> 31*
    47 -> 7,6,3,43,31
    52 -> 144,139,126
    54 -> 196,182,166,106,74
    56 -> 86,7,6,3,43,31
    63 -> 145*
    66 -> 7,6,3,43,31
    75 -> 45*
    78 -> 62*
    85 -> 77*
    86 -> 184,170,162,156,130
    87 -> 55*
    99 -> 63*
    101 -> 96*
    107 -> 63*
    112 -> 63*
    121 -> 109*
    129 -> 197,185,107,63
    131 -> 45*
    143 -> 197,185,107,63
    148 -> 197,185,107,63
    157 -> 63*
    165 -> 185,157
    167 -> 163*
    174 -> 185,157
    183 -> 171*
    188 -> 185,157
    197 -> 185*
  problem:
   
  Qed